A:Type, eq:EqDecider(A), f:fpf(A; a.top), g:top, x:A.
sqequal(fpf-ap(fpf-join(eq; f; g); eq; x);
sqequal(if fpf-dom(eq; x; f) then fpf-ap(f; eq; x) else fpf-ap(g; eq; x) fi ) 

latex

Definitions	x:A. B(x), fpf-ap(f; eq; x), fpf-join(eq; f; g), if b then t else f fi , t.2, fpf-cap(f; eq; x; z), t  T, P  Q, tt, ff, prop{i:l}, x. t(x), , Unit, P  Q, P  Q, x(s),
Lemmas	fpf-dom wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, top wf, fpf wf, deq wf